
#include <string.h>

static const int hex_chars[256] = {
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
     0, 1, 2, 3,  4, 5, 6, 7,  8, 9,-1,-1, -1,-1,-1,-1,
    -1,10,11,12, 13,14,15,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,10,11,12, 13,14,15,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
    -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1, -1,-1,-1,-1,
};

static inline int cli_hex2int(const char c)
{
        return hex_chars[(const unsigned char)c];
}


int main (int argc, char **argv) {

//int cli_hex2str_to(const char *hex, unsigned char *ptr, size_t len)
//{

   const char *hex; unsigned char *ptr; size_t len;

    size_t i;
    int c;
    unsigned char val;

    unsigned char ptr_val[16];
    const char hex_val[16];
    len = 16;
    
    klee_make_symbolic(&ptr_val, sizeof(ptr_val), "1");
    ptr = ptr_val;
    klee_make_symbolic(&hex_val, sizeof(hex_val), "2");
    hex = hex_val;


    for(i = 0; i < len; i += 2) {
        if((c = cli_hex2int(hex[i])) >= 0) {
            val = c;
            if((c = cli_hex2int(hex[i+1])) >= 0) {
                val = (val << 4) + c;
            } else {
                return -1;
            }
        } else {
            return -1;
        }
        *ptr++ = val;
//        *ptr = val;
    }

    return 0;
}

